feat(ownir): make the strict door accept the same language as the reference - #325
Conversation
📝 WalkthroughWalkthroughThe PR adds structured OwnIR errors, ordered raw-document validation, protocol validation, a generated 77-case Python fixture ledger, Rust parity replay tests, depth checks, and tolerant bridge deserialization. Migration records document validation status and remaining coordinate and depth-limit divergence. ChangesOwnIR validation and replay
Estimated code review effort: 4 (Complex) | ~60 minutes Possibly related issues
Possibly related PRs
Suggested reviewers: Sequence Diagram(s)sequenceDiagram
participant PythonOracle
participant FixtureLedger
participant RustReplay
participant OwnIrLoader
participant TolerantLowering
PythonOracle->>FixtureLedger: Generate validation cases
RustReplay->>FixtureLedger: Read expected verdicts and categories
RustReplay->>OwnIrLoader: Validate each JSON document
OwnIrLoader-->>RustReplay: Return acceptance or OwnIrErrorKind
RustReplay-->>FixtureLedger: Assert parity
TolerantLowering->>TolerantLowering: Deserialize raw facts
🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (1)
rust/crates/own-ir/src/lib.rs (1)
249-258: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueCorrect the doc link for the
columncheck location.The doc says the check lives in
OwnIr::validate. The check runs incheck_column, whichgate_componentscalls fromgate_semantics.OwnIr::validatedoes not inspectcolumn.📝 Proposed doc fix
- /// when the contract being violated is the 1-based coordinate rule. The - /// implementation mechanism must not pick the semantic category, so the - /// check lives in [`OwnIr::validate`] where it can answer `Location`. + /// when the contract being violated is the 1-based coordinate rule. The + /// implementation mechanism must not pick the semantic category, so the + /// check lives in [`gate_semantics`] where it can answer `Location`.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@rust/crates/own-ir/src/lib.rs` around lines 249 - 258, Update the `column` field documentation to reference `check_column` as the location of the semantic validation, noting its invocation through `gate_components` from `gate_semantics`; remove the incorrect `OwnIr::validate` reference while preserving the existing explanation.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/proposals/P-022-rust-core-migration.md`:
- Line 56: Update the typed OwnIR validation row to avoid claiming complete
coverage until the ledger adds controls for absent service.lifetime and
protocol-duplicate-name identity; alternatively, explicitly state these two
known measurement gaps in the row. Preserve the existing results and distinction
between the strict-door and tolerant-path checks.
In `@rust/crates/own-ir/src/lib.rs`:
- Around line 581-619: The service validation in gate_services must require and
validate lifetime before validating name, returning Vocabulary for an absent or
invalid lifetime while preserving the existing vocabulary message for invalid
values. Add service-lifetime-absent and order-lifetime-before-name controls in
tests/test_ownir_validation_fixtures.py (lines 251-289), then regenerate
tests/fixtures/ownir_validation.json; update rust/crates/own-ir/src/lib.rs
(lines 581-619) for the validation order and required field.
In `@tests/test_ownir_validation_fixtures.py`:
- Around line 340-346: The protocol-duplicate-name fixture lacks the
opens/closes fields required by the obligation parser, so its identity rejection
is not evidence for duplicate-name validation. In
tests/test_ownir_validation_fixtures.py lines 340-346, add the required fields
to both protocol records and regenerate the ledger; in
rust/crates/own-ir/src/lib.rs lines 663-687, retain gate_protocols only if the
regenerated ledger confirms the reference rejects duplicate names, otherwise
remove that gate to preserve Python/Rust parity.
- Around line 251-289: Add a services validation control that removes the
lifetime key after constructing the service with _svc, expecting a vocabulary
rejection. Add a second control with both an invalid or absent lifetime and an
invalid service name to pin the reference validator’s lifetime-before-name error
ordering, using the existing _c conventions and categories.
---
Nitpick comments:
In `@rust/crates/own-ir/src/lib.rs`:
- Around line 249-258: Update the `column` field documentation to reference
`check_column` as the location of the semantic validation, noting its invocation
through `gate_components` from `gate_semantics`; remove the incorrect
`OwnIr::validate` reference while preserving the existing explanation.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: c00d3440-1131-4127-855f-04738f7d46e1
📒 Files selected for processing (7)
docs/proposals/P-022-rust-core-migration.mdrust/crates/own-bridge/tests/replay.rsrust/crates/own-ir/src/lib.rsrust/crates/own-ir/tests/roundtrip.rsrust/crates/own-ir/tests/validation_replay.rstests/fixtures/ownir_validation.jsontests/test_ownir_validation_fixtures.py
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: af6e7824eb
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| fn gate_semantics(obj: &Map<String, Value>) -> Result<(), OwnIrError> { | ||
| gate_components(obj)?; | ||
| gate_services(obj)?; | ||
| gate_params(obj)?; |
There was a problem hiding this comment.
Validate every strict-door column
When functions[].params[].column is 0, or a nested operation in functions[].body has an invalid column, Python load() rejects it through _check_column/_check_flow_columns, but this semantic gate only checks parameter names and effects and never traverses function bodies. Because both columns remain in flattened extra maps, OwnIr::from_json returns Ok for documents the reference refuses.
Useful? React with 👍 / 👎.
| .and_then(Value::as_array) | ||
| .into_iter() | ||
| .flatten() | ||
| .filter_map(Value::as_object) |
There was a problem hiding this comment.
Reject malformed protocol records
When a protocol array contains a scalar or an object with an unknown matcher/event vocabulary, filter_map(Value::as_object) silently skips the scalar and the remainder of this gate checks only duplicate names; protocol_functions receives no record-level validation at all. Python load() calls parse_protocol/parse_method for every entry, so inputs such as {"protocols":[7]} or an unknown matcher kind are accepted only by the new strict door and may silently discard obligation facts.
AGENTS.md reference: AGENTS.md:L14-L14
Useful? React with 👍 / 👎.
| /// `protocols`. | ||
| fn gate_semantics(obj: &Map<String, Value>) -> Result<(), OwnIrError> { | ||
| gate_components(obj)?; | ||
| gate_services(obj)?; |
There was a problem hiding this comment.
Preserve section order before semantic gates
When an earlier section has a shape error and a later service has a semantic error—for example {"components":{},"services":[{"lifetime":"bad","name":"S"}]}—Python rejects the malformed components with Shape, while this call skips the non-array components and returns the service's Vocabulary error before serde performs the component shape check. Since OwnIrErrorKind is introduced as the parity contract and BR-D1 makes rejection order observable, semantic checks need to be interleaved with each section's shape validation rather than all running before deserialization.
Useful? React with 👍 / 👎.
| // trap the reference guards explicitly (a Python `bool` is an `int`, so | ||
| // `True` would otherwise be read as column 1 — a fabricated coordinate). | ||
| let ok = match v { | ||
| Value::Number(n) => n.as_i64().is_some_and(|i| i >= 1), |
There was a problem hiding this comment.
Avoid narrowing valid columns to i64
When a positive JSON column exceeds i64::MAX, serde_json represents it as an unsigned number and as_i64() returns None, so this check rejects it as a location error. Python JSON integers are unbounded and _check_column accepts every integer greater than zero, meaning a document such as {"components":[{"subscriptions":[{"column":9223372036854775808}]}]} was valid in the reference but is now rejected by Rust, violating the claimed zero Rust-only-reject parity.
Useful? React with 👍 / 👎.
All seven findings are real. cp1 is not complete, and the row now says so (
|
|
@coderabbitai review |
✅ Action performedReview finished.
|
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@rust/crates/own-ir/src/protocol.rs`:
- Around line 276-332: Update the events validation flow centered on events to
track recursive depth across if then/else and while body branches, and reject
trees exceeding an explicit bounded limit before further recursion. Thread the
counter through every recursive call while preserving existing event-shape and
per-kind validation behavior, ensuring OwnIr::validate() cannot accept
excessively deep in-memory protocol trees.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 11016f26-d0dd-40ec-9535-144fbb4c0a3f
📒 Files selected for processing (7)
docs/proposals/P-022-rust-core-migration.mdrust/crates/own-ir/src/lib.rsrust/crates/own-ir/src/protocol.rsrust/crates/own-ir/src/strict.rsrust/crates/own-ir/tests/validation_replay.rstests/fixtures/ownir_validation.jsontests/test_ownir_validation_fixtures.py
…in §4.2 Two review findings on bc8790c, both real, one with a wrong consequence attached. **The schema had to carry the bounds too.** `spec/ownir.schema.json` is what a NON-Python consumer validates against. With the bounds only in `load()`, a producer could be schema-valid and still refused at the door — the same cross-consumer mismatch this change exists to remove, one layer further out. Added `$defs.sourceLine` (signed-64) and a `maximum` on `sourceColumn`, and rebound all 21 inline `"line": {"type": "integer"}` fields to it. The test now asserts the schema's four numbers against the same literals as the code, so the two cannot drift. Mutation-proved both ways: widening `sourceLine.maximum` to `2^64-1` and dropping `sourceColumn.maximum` are each caught. **§4.2 said "every `line`" and two line-bearing fields escaped it.** The finding is right that the sentence overclaimed. Its stated consequence — that this "preserves the Python/port divergence" — is not: measured, both implementations accept those fields, because neither types them. python subscription line 2^80 : ACCEPT rust: ACCEPT python subscription line "x" : ACCEPT rust: ACCEPT python flow op line 2^80 : ACCEPT rust: ACCEPT python flow op line "x" : ACCEPT rust: ACCEPT `components[].subscriptions[].line` and the `line` on a flow op inside `functions[].body` are checked NOWHERE by `load()` — not for range, and not even for type. #325's validator has no check for them either (grep `"line"` in strict.rs: services, effects, bindings, params, sites — not these two). So this is not a parity gap, and closing it is not part of removing one. It is a separate contract question: whether a coordinate no rule reads should nevertheless have to be well-formed. Extending the check would be a new restriction on documents accepted today, arriving inside a PR whose job is to close a measured divergence — so §4.2 now enumerates exactly the fields it enforces, marks the word "validated" as load-bearing, and records the two exceptions with the measurement instead of quietly widening or quietly overclaiming. Corpus scan for the record: 150 JSON files, zero offenders on either path, so extending it later would break nothing in the tree. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
|
@coderabbitai review
Generated by Claude Code |
|
Your plan includes PR reviews subject to rate limits. More reviews will be available in 1 minute. |
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (1)
rust/crates/own-ir/tests/validation_replay.rs (1)
337-377: 🎯 Functional Correctness | 🔵 Trivial | ⚡ Quick winTest the actual parser boundary.
Line 347 says this test builds the deepest document that
OwnIr::from_jsonaccepts. It builds only 50 wrappers.A lower depth guard can still accept this fixture while rejecting a deeper document that the parser accepts. Generate valid documents up to the first
from_jsonrejection, then requireto_value()to accept the last successful document. This pins the no-new-rejection contract.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@rust/crates/own-ir/tests/validation_replay.rs` around lines 337 - 377, Update the test the_depth_guard_never_fires_on_a_document_from_json_accepts to determine the actual OwnIr::from_json boundary instead of using a fixed 50-level fixture: generate progressively deeper valid documents, retain the deepest successfully parsed document, stop at the first parse rejection, and assert that the retained document’s to_value() succeeds. Preserve the existing ledger-control checks.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/proposals/P-022-rust-core-migration.md`:
- Line 76: Update the line beginning with “#260/#269” in the proposal so it no
longer starts with a Markdown heading marker; prefix it with “issues” or move
the text onto the preceding line while preserving the existing meaning.
- Line 56: Reconcile the matrix figures in the P-022 checkpoint with the PR
objective totals: update “31/162” and “31 mutations” to the agreed “29 accepts,
162 rejects, and 27 mutations,” or explicitly label the existing figures as
pre-exclusion totals and state how the two excluded divergence families account
for the difference.
---
Nitpick comments:
In `@rust/crates/own-ir/tests/validation_replay.rs`:
- Around line 337-377: Update the test
the_depth_guard_never_fires_on_a_document_from_json_accepts to determine the
actual OwnIr::from_json boundary instead of using a fixed 50-level fixture:
generate progressively deeper valid documents, retain the deepest successfully
parsed document, stop at the first parse rejection, and assert that the retained
document’s to_value() succeeds. Preserve the existing ledger-control checks.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 51d9b94d-f32a-4ce1-aad7-1f5e59adc67d
📒 Files selected for processing (8)
docs/proposals/P-022-rust-core-migration.mddocs/proposals/README.mdrust/crates/own-ir/src/lib.rsrust/crates/own-ir/src/protocol.rsrust/crates/own-ir/src/strict.rsrust/crates/own-ir/tests/validation_replay.rstests/fixtures/ownir_validation.jsontests/test_ownir_validation_fixtures.py
🚧 Files skipped from review as they are similar to previous changes (1)
- tests/test_ownir_validation_fixtures.py
| | #259 checkpoint | Status | Evidence / what remains | | ||
| |---|---|---| | ||
| | 1 — typed OwnIR validation | **partial** | `OwnIr::from_json` + the #294 OD-2 fail-loud unknown-kind rule. Full validation acceptance/rejection parity (fixture layer 1) is out of the current slice | | ||
| | 1 — typed OwnIR validation | **acceptance surface closed except two named families — not yet complete** | Two censuses. The first froze 77 controls, closed twelve permissive documents and read 0/0/0 — then review found seven divergences the ledger could not express, because the same author wrote the ledger and the port and one gap in reading BR-D1 produced a matching gap in each (`_svc()` always supplied `lifetime`, so no control could omit it). The re-census is derived from `load()` and `obligations.py` line by line: **193 controls**, which opened a further **58** permissive documents and **9** category mismatches. Closing them was architectural — the strict door is now a sequential validator over the raw document (`own-ir/src/strict.rs`) reproducing BR-D1's interleaving of shape and semantics *per section, in declaration order*; `serde` is the typed constructor, and a document it rejects after validation is reported as a hole in the validator and asserted against. The obligation **acceptance grammar** is ported (`own-ir/src/protocol.rs`); protocol *analysis* is not, and is not part of what the door accepts. Taxonomy is now **seven** categories: `WellFormedness` was added for the two protocol rules whose values are all correctly typed and whose records still cannot mean anything — a category set frozen by the first census is a claim about that census, not about the contract. Matrix 31/162, 0/0/0; 31 mutations each caught, five only by the validator-hole guard and two changing nothing but a category. **Why this is not yet complete:** two Python-accept/Rust-reject families are measured and deliberately excluded from the ledger — source coordinates beyond Rust's integer range, and sufficiently deep protocol/flow nesting. 0/0/0 therefore means "over a set from which two known divergence families were removed", which is not the parity #259 asks for. Both close in one **Python-first** defensive-limit change (signed-64 coordinates; one measured domain nesting limit, at-limit accept and limit+1 reject, written into the OwnIR contract). That lands first; this checkpoint is then rebased, gains boundary controls for both families, and is re-measured before it may be called complete. #294 OD-2 remains a separate tolerant-door concern | |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Reconcile the reported matrix totals with the final results.
Line 56 reports 31/162 and 31 mutations, but the PR objectives report 29 agreed accepts, 162 agreed rejects, and 27 mutations. Update these values, or label the current values as pre-exclusion totals and explain the difference.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/proposals/P-022-rust-core-migration.md` at line 56, Reconcile the matrix
figures in the P-022 checkpoint with the PR objective totals: update “31/162”
and “31 mutations” to the agreed “29 accepts, 162 rejects, and 27 mutations,” or
explicitly label the existing figures as pre-exclusion totals and state how the
two excluded divergence families account for the difference.
#326) Two OwnIR shapes had no bound at all, and the reference accepted both because *Python* has none: arbitrary-precision integers, recursion limited only by the interpreter stack. That is not generosity, it is an accident of the reference's implementation leaking into the contract — a vocabulary implementable only in a language with bignums and a deep stack. It surfaced as a measured Python-accept/Rust-reject pair in #259 cp1. The honest reading is not "the port is over-strict", so the fix is Python-first, per the standing migration rule: a Rust/Python divergence is a Rust bug UNLESS behaviour changes in a separate Python-first PR. This is that PR. Source coordinates fit a signed 64-bit integer. Every *validated* line — services[].line, ctor_line, root_resolve_sites[].line, scope_cache_sites[].line, effects[].line, bindings[].line, params[].line, protocol_functions[].events[].line — lies in [-2^63, 2^63-1]; every column is 1..=2^63-1, or absent, or null. The word "validated" is load-bearing and the exception is recorded rather than papered over: components[].subscriptions[].line and the line on a flow op are checked NOWHERE by load(), not even for type. Measured, {"line": "x"} is accepted by both implementations, so it is not a parity gap, and closing it is not part of removing one. §4.2 records it as a separate open contract question. Corpus scan: 150 files, 0 violators. Flow bodies and protocol event trees nest at most 32 levels, derived by measuring both ends: the deepest nesting in any fixture here is 3, and a parser applying the common 128-level recursion cap stops accepting these documents at 62, because each `if` costs two JSON levels. The limit is stated in the OwnIR domain — nested bodies — not in JSON levels. Both bounds are strict-door rejections, not coercions; check_facts() keeps its degrade-to-absent behaviour. spec/ownir.schema.json carries the same numbers, because it is what a non-Python consumer validates against: bounds living only in load() let a producer be schema-valid and still be refused at the door. The binding map is asserted AS a map — bound where load() checks, unbound where §4.2 records that it does not. Mutation campaign: 18 mutations, 15 caught, 1 invalid, 2 survived — and the two survivors are the same error in two places. The test IMPORTED the constants it checked, so every boundary case moved with them: it could prove the limits were applied consistently and could not prove they were right. And the binding map checked `ref != sourceLine`, knowing exactly one way to be narrow, so pointing flowOp.line at sourceColumn or giving it an inline maximum both passed. Spec numbers are literals now, and the whole subschema is kept. Both found by mutating, neither by reading: a test written in terms of the value under test asserts self-consistency, not correctness — the same failure the cp1 ledger had one layer up. The off-by-one was measured too, not reasoned: _check_flow_columns probes every op for then/else/body whether or not it has them, so checking depth before the early return counted the absent ones and rejected a body at exactly the limit. Only the at-limit case caught it, which is why each limit is pinned at three points — below, exactly at, and one past. Unblocks #325 (#259 cp1): until these bounds exist, cp1's 0/0/0 is a result over a set with two known divergence families removed from it. Refs #250, #259.
#259 checkpoint 1, census step. The Python-authored oracle only — the Rust replay and the fixes it will force come next, deliberately after the measurement rather than alongside four hand-picked repairs. 77 controls over every BR-D1 rejection family, each with a neighbouring valid twin so the rejections are discriminating rather than passing against a loader that refuses everything. 10 accept / 67 reject across six categories. What is compared: accepted/rejected, and on rejection the CATEGORY. Not the message text — #259 asks for a matching error class/category, and Python funnels every rejection into one OwnIRError whose strings are a human-facing presentation aid. Byte-comparing them would freeze a debug surface as a cross-language contract. The taxonomy is deliberately small and derived from mechanisms, not messages: json / version / shape / vocabulary / identity / location. A category with no control that exercises it fails the ledger, so the taxonomy cannot outgrow its evidence. `reference` is absent on purpose: the sweep found no load-time referential constraint, and adding it on the strength of the issue text alone would invent a category nothing can exercise. BR-D1 fixes the ORDER of checks and notes it is observable through which error fires first, so six order-discrimination controls violate two rules at once. Each has exactly one correct category; a loader running its checks in a different order reports the other and fails. Found while building it: the ledger was non-deterministic on the first regeneration. `load()` takes a path and splices it into two of its messages, so a temporary filename rode into the golden. Normalized to a fixed token, and determinism is now asserted rather than assumed — a golden that changes every run cannot detect anything. Refs #259, #250. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
…erence #259 checkpoint 1, implementation. The census (5030314) opened at 12 Rust-only accepts; this closes them and makes the crate's long-standing claim to "mirror the acceptance of Python load exactly" true for the first time. Matrix over the 77-control ledger, all three failure rows required zero: python accept / rust accept : 10 python reject / rust reject : 67 (same category) python reject / rust ACCEPT : 0 (was 12) python accept / rust REJECT : 0 category mismatch : 0 (was 5) Four mechanisms, not twelve special cases: * SIX fields were not declared in the Rust model at all (`source_provenance`, `ignore_reason`, `sig`, `column`, `protocols`, `protocol_functions`), so they fell into serde(flatten) `extra` and escaped checking. serde is admirably strict about fields it has been told about. Each is declared with ITS OWN semantics — `resource` rejects null, the nullable-optionals accept it — not one blanket policy, since sharing a bug is not sharing a contract. * the 1-based column rule (#317): 0, negative, bool and string. * the closed `resource` vocabulary (IR4). * protocol-name identity. Errors are now typed. `OwnIrErrorKind` = Json | Version | Shape | Vocabulary | Identity | Location, one variant per mechanism a loader can reject on. The ledger fails if a declared category has no control exercising it, so the taxonomy cannot outgrow its evidence — which is why there is no `Reference` variant: the sweep found no load-time referential constraint. Category is compared, message text never is. The reference funnels everything into one OwnIRError whose strings are a presentation aid. Equally, the expected category is DECLARED by the ledger and confirmed by the oracle only as accept/reject — deriving it from Python's message would abandon message parity at the front door and rebuild it as regex parity at the back. The mechanism must not pick the category. A serde enum would reject `lifetime: "eternal"` perfectly well and call it Shape, when the contract is a closed vocabulary; a typed NonZeroU32 column would call a 0 Shape when the contract is a coordinate. So vocabulary/identity/location run in a gate over the RAW document before deserialization — which also gets the BR-D1 order right, where the version gate must precede shapes. Both doors keep their unknown-resource check. The strict door now rejects at load (cp1); the lowerer keeps its own (#294 OD-2) because the tolerant path bypasses `load()` entirely. This became load-bearing immediately: the bridge's `tolerant_unknown_kind` fixture was routing through `from_json`, so a strict door that enforces IR4 made the tolerant-door test unreachable. It now deserializes directly, as its real callers do. Seven mutations, one per mechanism plus one that only misclassifies a category while still rejecting — all caught. That last one is the guard against a decorative taxonomy. P-022's cp1 row corrected: it conflated the two doors, reading as though OD-2 satisfied cp1. Refs #259, #250. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
…the port
Independent review found seven divergences the 77-control ledger cannot see, so
the 0/0/0 matrix was true only over the controls I wrote. Each verified against
the reference before recording:
absent service.lifetime python reject / rust ACCEPT
params[].column: 0 (+ flow body) python reject / rust ACCEPT
protocols: [7], malformed records python reject / rust ACCEPT
column > i64::MAX python ACCEPT / rust reject <- over-strict
components shape vs later service semantics Shape vs Vocabulary
lifetime-before-name order reference checks lifetime first
protocol-duplicate-name control rejects on record shape, not the duplicate
Two are structural rather than missing branches.
Ordering: BR-D1 interleaves shape-then-semantics per section. This port runs
every semantic check before deserialization, which got the version gate right
and everything after it wrong — `{components:{}, services:[{lifetime:"bad"}]}`
answers Vocabulary where the reference answers Shape. Fixing it means
interleaving per section, not adding another check.
Range: Python integers are unbounded and `_check_column` accepts any positive
one. `as_i64()` returns None above i64::MAX, so a document the reference accepts
is rejected. The over-strictness row was never actually zero.
The honest lesson is about the ledger, not the port. I wrote both, so a gap in
my reading of the contract produced a matching gap in each, and the matrix read
green — `_svc` always set `lifetime`, so no control could ever omit it. A
same-author oracle measures the author's understanding, not the contract. The
reviewers found these precisely because they were not the author.
The claim is corrected before the fixes land rather than after, so the PR does
not sit on a false "complete" while the work is done.
Refs #259, #250.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
… port
The first census reached 0/0/0 over 77 controls and was recorded as
complete. Review then found seven divergences it could not express.
The cause was structural, not careless: the same author wrote the oracle
and the port, so one gap in reading BR-D1 produced a matching gap in
each and the matrix agreed with itself. The sharpest instance is
`_svc()`, which always supplied `lifetime` — so no control could omit
it, and the reference rejects an absent lifetime while the port accepts
it. Mutation testing proved the implementation against the ledger.
Nothing proved the ledger against the contract.
So this round is derived by reading `load()` and the shared obligation
parser line by line, before looking at what the port does with them.
191 controls, up from 77.
New families:
- required fields ABSENT (the `_svc()` blind spot), plus `_proto()`
and `_pfn()` helpers that build deliberately incomplete records
- ordering WITHIN a section: lifetime-before-name, sig-before-body,
body-columns-before-params, param name/line/column/effect
- ordering ACROSS sections: BR-D1 interleaves shape and semantics per
section, so a components SHAPE failure outranks a services
VOCABULARY failure. Six controls chain every section boundary
- flow columns, recursive through then/else/body to three levels
- params[].column, a separate reference call site the port lacked
- the protocol acceptance grammar delegated to obligations.py:
parse_protocol / parse_matcher / parse_events / parse_method,
with valid twins first — the old duplicate-name control used
records with no opens/closes, so it never reached the duplicate
branch it claimed to test
- explicit null on every section and scalar (present null is not
absent), and the three places where null IS accepted
- integer boundaries pinned at i64::MAX, where both sides agree
Measured RED at this commit, all three rows in one reading:
agreed accept 29
agreed reject 95
python reject / RUST ACCEPT 58
python accept / rust reject 0
category mismatch 9
The nine mismatches are the architecture, not nine oversights: absent
required fields surface as serde `Shape` instead of the contract's
vocabulary/identity, and "all semantics, then all shapes" inverts
precedence both within and across sections.
The replay now reports all three failure rows in one assertion instead
of three sequential ones. Sequential asserts show only the first
non-empty row, which is how a 58-and-9 census would have read as a
permissiveness problem alone.
Integer width is measured and deliberately NOT covered: Python ints are
unbounded and every line/column field accepts values past 64 bits, so
Rust is over-strict across seven field families. Widening Rust to
arbitrary precision to honour a nine-quintillion source coordinate is
the wrong repair; the boundary is pinned where both agree and the range
above it is a separate Python-first defensive limit.
No production code changed in this commit.
Refs #250, #259.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
Closes the 58 permissive documents and 9 category mismatches the
re-census opened. The fix is architectural: no arrangement of the
previous design could have passed.
The previous door ran `version gate -> all semantic gates -> serde for
all shapes`. That is a third check order, matching neither
implementation. BR-D1 validates each section COMPLETELY before the next
begins, interleaving shape and semantics inside it — so a `components`
shape failure outranks a `services` vocabulary failure, and within a
service `lifetime` outranks `name`. Hoisting semantics in front of serde
gets section-local controls right and every ordering control wrong.
So the strict door is now a sequential validator over the raw document:
own-ir/src/strict.rs primitives + one function per section, applied
in the reference's order
own-ir/src/protocol.rs the obligation ACCEPTANCE grammar
Not 47 transcribed `if`s — eight primitives, each encoding one of
Python's access idioms, and section validators that apply them:
objects / list d.get(k, []) as a container
name_slot isinstance(v, str) and v — a value facts join on
optional_string `is not None and not isinstance` — null tolerated
defaulted_string isinstance(d.get(k, "?"), str) — null rejected
defaulted_int int and not bool
string_array list of str
column the 1-based contract (#317), recursive over flow
sites the {type, file, line} record
The two string primitives are the place a single "policy for optional
fields" would be silently wrong: `resource` rejects an explicit null and
`source_provenance` accepts it, because the reference writes one as a
defaulted isinstance and the other as `is not None and ...`.
serde is now the CONSTRUCTOR, not the arbiter. Once the validator
accepts, a serde failure means a rule lives in the model rather than the
validator — its category and its ordering would both be accidental. That
is marked with a sentinel and asserted against by
`no_control_escapes_into_serde`, which is not decoration: five of the 27
mutations below are caught by it ALONE, because the model still enforced
the rule while the validator no longer did.
`OwnIr::validate` is now `to_value` + the same validator. It costs a
round-trip and buys single-copy-of-the-law — the property whose absence
already produced a false "mutation survived" in this PR, when a planted
mutation hit one copy of a duplicated check and the other caught it.
Protocol scope, exactly as agreed: `parse_protocol`, `parse_matcher`,
`parse_events`, `parse_method` — what the door ACCEPTS. Not the
lattice, the walker, matching, or verdicts. `protocols` and
`protocol_functions` stay raw `Value`s with pure validation beside them,
because nothing consumes a typed representation yet. Two of the grammar's
rules ("can never fire", "barrier equals opens") are well-formedness
rather than shape; they are recorded as `shape` with the taxonomy strain
written down rather than a seventh category invented unilaterally.
Final matrix over 191 controls:
agreed accept 29
agreed reject 162
python reject / rust accept 0
python accept / rust reject 0
category mismatch 0
27 mutations, all caught — one per mechanism, plus three that only
change a category while still rejecting, plus two that only change
ORDER. The order mutations matter most: they are the ones the previous
architecture could not have failed.
Also fixed: `is_none_or` needs Rust 1.82 and the workspace MSRV is 1.74;
three `private_intra_doc_links` of the same class #324 hit; and the
replay now reports all three failure rows in one assertion, since
sequential asserts showed only the first and would have made this a
two-round discovery.
Still open and deliberately not closed here: Python integers are
unbounded, so every line/column field accepts values past 64 bits and
Rust is over-strict above i64::MAX across seven field families. The
ledger pins the boundary where both agree. The range above it is a
Python-first defensive limit, not a reason to thread arbitrary-precision
integers through own-ir and the bridge.
Refs #250, #259.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
The proposals index named lowering and MOS but not validation, so the third surface disagreed with the other two the moment cp1 landed. P-022 and #250 were updated in the same change (#250 via the API, no git commit): the status-drift rule says the surfaces move together. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
…walk Review finding on e5f52e8: `OwnIr::validate()` can be handed an arbitrarily deep in-memory value, and nothing stops the recursion. Real, and introduced by this PR — before e5f52e8 `validate()` did not recurse at all. The proposed fix was a depth counter threaded through `events`. Measured against the tree, that would have been dead code. Binary search on the same tree: to_value() survives to ~831, aborts by ~846 validate() survives to ~831, aborts by ~846 Identical, because `validate` serializes first. The stack dies inside `serde_json::to_value` before the validator's own recursion is ever reached, so a counter in `events`/`flow_columns` could never be the check that fires. The bound has to run BEFORE serialization. So the guard is in `to_value`, which already returns `Result`: - `strict::check_depth` measures depth with an EXPLICIT STACK. A recursive depth check would be the failure it is meant to prevent, and would abort rather than return — a stack overflow is not catchable. - `OwnIr::check_raw_depth` walks the raw values the model carries (`extra` maps, both protocol sections, `Subscription::column`) with plain loops; typed nesting is fixed-depth, so no recursion there. - The limit is 128, serde_json's own parse limit. A document that could be PARSED never exceeds it, so this rejects nothing `from_json` accepts. `from_json` was never exposed: serde_json caps nesting at 128 and refuses around 120 event levels. HONESTY NOTE, measured not assumed: this covers depths 129..~800. Above ~804 merely DROPPING the value aborts, because `serde_json::Value` has a recursive `Drop` — nothing this crate does can prevent that, and a test asserting otherwise aborts before it can report. The first version of the regression test used depth 900 and died in `Drop`, which is how the band got measured. The guard stops the serializer, not the type. Also corrected: two doc comments claimed recursion was "bounded by serde_json's 128-level parse limit". True for `from_json`, false for a value built in memory — which is precisely the gap the finding names. Four mutations, all caught — but only after fixing the second test. `the_depth_guard_never_fires_on_a_document_from_json_accepts` originally ran over the ledger alone, and every control is a few levels deep, so tightening the guard to 16 SURVIVED. It now builds the deepest document `from_json` still accepts (50 nested events, ~105 JSON levels) and pins the guard above it. Same lesson as the census: a test that cannot distinguish the mutation is not evidence, whatever it asserts. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
Recounted from the fixture rather than from memory: of the 58 permissive documents the second census opened, 47 are protocol-grammar cases (`protocols`, `protocol_functions`, and their two ordering families) and 11 are the flow/param column families. A wrong number in a module doc that exists to justify a scope decision is worse than no number. Refs #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
Veto on filing two protocol rules under `shape`, and the reasoning behind the veto is the part worth keeping. `protocol can never fire` (no barriers with `exit_barriers: false`) and `barrier == opens` were reported as `Shape` while the code comment directly above them said "both are well-formedness, not shape". Every value in such a record has the right type and a legal vocabulary; what is broken is that the record cannot MEAN anything. The justification given was that the taxonomy was already frozen at six. That is backwards. The taxonomy was frozen by the FIRST census; this mechanism was found by the SECOND — the same census that just proved a category set settled early is a claim about the settling, not about the contract. Filing a newly discovered mechanism under the nearest existing name is the exact substitution this enum was built to stop, and it was the substitution being made. So: `OwnIrErrorKind::WellFormedness`, wire name `well_formedness`. Both rules move to it. The enum's doc now states the set is closed by measurement in BOTH directions — it cannot outgrow its evidence (no `Reference` variant, nothing reaches it) and it is not frozen against new evidence. Ledger: 191 -> 193 controls. The two new ones are the acceptance twins the category needs — `exit_barriers: false` WITH a barrier, and a barrier that differs from `opens` — so the rejections are about meaning rather than about the fields being present at all. Four mutations, all caught, including the two that matter most here: each rule reported as `Shape` while still rejecting. Category-only mutations are the only thing that can tell a real taxonomy from a decorative one. Also, per review: 128 is now the ONLY normative depth number. The measured abort points (~831/~846 for serialization, ~804/~851 for `Drop`) are properties of one stack size, build profile and platform. They are good forensics and they were creeping into doc comments as if they were specification; they are out of the normative wording and the PR keeps them as evidence. And the guard's promise is stated precisely instead of absolutely. It was "nothing this crate does can prevent that". Correctly: `to_value()` and `validate()` refuse a too-deep value and RETURN rather than aborting inside the serializer. They do not promise that any `Value` a caller built is safe to hold — `serde_json::Value` has a recursive `Drop`. Guaranteeing that would mean not representing facts as `serde_json::Value`, a representation change and outside cp1. Status, per the same review: cp1 is NOT complete and P-022 + the index now say so. 0/0/0 currently means "over a set from which two known Python-accept/Rust-reject families were removed" — coordinates beyond Rust's integer range, and deep nesting. That is not the parity #259 asks for. Both close Python-first, before this checkpoint may be called complete. #250 is corrected in the same logical change, via the API. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
Review raised one of these as a nitpick against `af6e782`. Checking it
against the current tree found four more, all mine, all introduced by
not re-reading doc comments after the architecture changed under them.
* the crate doc still said the ledger was **191** controls; the
seventh category took it to 193. Same number stale in the depth test.
* `Subscription::column` said the check "lives in `OwnIr::validate`".
It lived in `gate_components` when that was written, and both are
gone: it is `strict::column`, reached from `from_json` and
`validate` alike.
* `OwnIr::protocols` was the bad one. It still read "Record-level
validity beyond that is NOT yet mirrored" — the exact claim this PR
retracted. The reference CALLS the obligation parser inside `load()`
and wraps its errors, so it is part of the door, and the second
census measured that supposed boundary as 47 of its 58 permissive
documents. The comment was describing the bug as if it were the
design.
* `OwnIr::protocol_functions` repeated it by reference.
Worth naming: the misleading one was not the one review found. It was
found by grepping for every stale symbol at once — `gate_*`, `191`,
`OwnIr::validate` — rather than fixing the line that was pointed at.
A doc comment that survives the code it documents is the same failure
class as a test that survives the behaviour it asserts; neither gets
re-read just because something near it changed.
Refs #250, #259.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
Review nitpick, and it is the same failure as the last three: the depth test asserted something weaker than it claimed. It built a FIXED 50-wrapper document and said it was "the deepest document `from_json` still accepts". It was not — the parser reaches ~61 wrappers. Any guard between the two passes the test while rejecting documents the door accepts, which is precisely the new-rejection-rule the test exists to forbid. Measured, by restoring the old shape and mutating against both: guard 55 fixed-50: caught discovered: caught guard 105 fixed-50: PASSES discovered: caught So the boundary is now discovered rather than sampled: walk depth upward until `from_json` refuses, keep the deepest document it accepted, and require that one to survive `to_value`. That states the contract exactly — "the guard never fires on anything the parser accepts" — instead of picking a depth that happens to sit under it. Three guard mutations caught (55, 105, and 16 as a regression). Also fixed, from the same review: `#260/#269` opened line 76 of P-022 and markdownlint read it as an ATX heading (MD018). Same class as the one caught in #322; reflowed. DECLINED, with the measurement: the review also asked to reconcile P-022's "31/162, 31 mutations" against the PR body's "29/162, 27". The direction is inverted — P-022 is right and the BODY is stale. Measured: ownir validation ledger OK: 193 controls (31 accept / 162 reject) 31 accepts and 162 rejects is the post-`WellFormedness` ledger, and 31 mutations is 27 plus the four that category needed. The PR body still carried the pre-seventh-category numbers; it is corrected there rather than by editing the correct figures to match the wrong ones. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
Measured RED. No production code in this commit — the point is the number before the fix, and a fix landing beside its own evidence cannot be checked against it. #326 closed both families Python-first, so the reason for excluding them is gone. The previous census reported 0/0/0 over a set from which the two places the implementations were known to disagree had been removed. That is a true statement about a chosen subset, not the parity #259 asks for, and the honest way to find out what it was hiding is to put the cases back. 193 controls -> 216. The three mechanisms it opens are distinct: matrix: agreed_accept 35, agreed_reject 166, rust_only_accept 7, rust_only_reject 0, kind_mismatch 8 plus 8 controls escaping into serde (VALIDATOR_HOLE) Eight `line` paths escape into serde. `is_integer()` answers "is this an integer" and `i64::MAX + 1` still is one to the parser, so the raw layer waves it through and the typed model refuses it afterwards. The rule was living in the model rather than in the door, which makes both its category and its ordering accidental — exactly what the sentinel exists to name. It fires on services line, ctor_line, both site arrays, effect, binding and param. Seven documents the reference refuses are ACCEPTED by the port: all six nesting-past-limit controls, since the port has no depth rule at all, and `event-line-above-i64`, which does not even reach the sentinel — protocol events are stored raw, so serde never gets a chance to refuse the value and the document is analysed with a coordinate no consumer can hold. Eight controls reject on both sides and disagree about why, and this is the finding worth the most. `column` was reading its category off the reference's DIAGNOSTIC rather than off the mechanism: `_check_column` raises one message for a bool, a string, a float, an out-of-range integer and a zero alike, and the ledger inherited that single message as a single category. So a bool column was `location` — a "1-based contract violation" for a value that has no integer form for the 1-based rule to be about. The conflation was visible in the file and read as intent. `column-float` was `location` and `line-float` was `shape`, adjacent, with a comment explaining that a float column and a float line "are the same, where it is a shape failure instead". One violation, two categories, documented as a decision. The taxonomy is therefore split along the axis it was always missing: shape the value has no representable primitive or container form the contract requires location a REPRESENTABLE coordinate violating its coordinate-domain rule, currently the 1-based column `representable` is load-bearing and belongs to OwnIR, not to serde: `i64::MIN - 1` is `shape` because §4.2 declared signed-64 the representable integer form, not because a parser turned it into a float. Measured, the parser reaches these values by two routes — `i64::MAX+1 ..= u64::MAX` materialises as u64, anything outside `i64::MIN ..= u64::MAX` drops to f64, and there is no negative u64 band, so the two ends are not mirror images. Recovering the lost token would need `arbitrary_precision`. One category over both routes removes the need to, and refuses to let the parser's materialisation choose the semantics. Six existing controls move `location` -> `shape`. Nothing else about them changes: Python's accept/reject is untouched, its message text is untouched, and the reference is not edited in this commit or the next. Only our cross-language classification of the cause moves. Checked before doing it, because the risk was real: all four cross-category `order-*` controls use `column: 0`, so they stay genuine `location` controls and the BR-D1 ordering evidence survives the split intact. A taxonomy fix that had quietly turned `location`-before-`vocabulary` into `shape`-before-`shape` would have bought a cleaner enum with a vacuous ordering proof. Three of the new coordinate controls are green on arrival — `line-below-i64`, `line-above-u64` and `line-float` already reject as `shape`, because they take the f64 route into the same branch as a plain float. They are kept as regression guards for the half of the range that was accidentally right. Precedent for changing the taxonomy on new evidence is the taxonomy's own: `WellFormedness` was added when the nearest existing category was found inadequate. A category set that survives one census is a claim about that census. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
GREEN for the RED measured in the previous commit. 216 controls, matrix
35 / 181 / 0 / 0 / 0, no control escaping into serde.
Three mechanisms, one idea: the strict door decides what a value IS before
anything decides what it MEANS.
`is_integer` becomes `is_representable_int` and narrows from
`is_i64() || is_u64()` to `is_i64()`. That is not an extra check bolted beside
the type check — it IS the type check, finally stated at the width OwnIR has.
The old predicate answered "is this an integer at all", which `i64::MAX + 1`
satisfies, so the raw layer waved it through and the typed model refused it
afterwards. Because the predicate is shared, all eight validated `line` paths
close at once, and `sites` and `column` close with them.
`column()` splits into four outcomes in order: absent or null accepts,
unrepresentable is `Shape`, representable-and-below-1 is `Location`,
representable-and-at-least-1 accepts. It is the only field carrying both axes,
which is why it is where they were conflated — one predicate reported a bool,
a string, a float and an out-of-range integer as a "1-based contract
violation", for values with no coordinate in them for the rule to be about.
Nesting gets the contract's own domain limit, mirrored from the reference
rather than chosen here. Two recursions, and deliberately not symmetrical: the
flow walker checks depth AFTER the early return, the event walker BEFORE the
list check. That is not sloppiness, it is the reference — a missing event arm
is read as `e.get("then", [])` and still descends a level, while the flow
walker probes for a key that may not be there and must not count what it did
not find. Mutating either into the other's shape is caught.
`OwnIrErrorKind::Shape` and `::Location` are re-documented around the word
representable, because that word is what makes the split a contract rule
instead of an implementation detail: `i64::MIN - 1` is `Shape` because §4.2
declared signed-64 the representable form, not because serde_json flattened it
to a float on the way in.
The depth witness had to move, and finding out why is the most useful thing in
this commit. `the_depth_guard_never_fires_on_a_document_from_json_accepts`
nested a protocol event tree and walked until `from_json` refused. Correct
while nothing bounded that tree — and the nesting rule above bounds it. So the
walk started stopping at the door instead of at the parser, and the assertion
quietly degraded from "the guard is looser than the parse ceiling" to "the
guard is looser than 32". Measured, immediately after the rule landed:
witness = event tree deepest 32, terminating error Shape
witness = unknown top section deepest 62, terminating error Json
Two halves to the fix. The witness moves to an unknown top-level section,
which the door tolerates by design and the ledger pins. And the walk now
ASSERTS that what stopped it was `OwnIrErrorKind::Json`. Only the second half
generalises: picking an unbounded witness is a fact about today's rules, and
the last witness stopped being one without saying so. Now any future rule that
shadows the parse boundary fails here, naming its own kind.
The schema binding map is closed over `$defs` the same way. It checked the
defs it already named, so a coordinate-bearing def added later would be in
neither BOUND nor UNBOUND and checked by nothing, while the test went on
passing — an assertion proving the completeness of a list, using the list.
Discovery now walks `$defs` and the two sets must be equal.
Mutation campaign: 17 mutations, 17 caught.
1 is_representable_int widened back to u64
2 column's representability branch removed
3 representability answers Location instead of Shape
4 flow depth off-by-one
5 flow depth never fires
6 flow depth not threaded through then/else/body
7 flow depth check moved BEFORE the early return
8 event depth off-by-one
9 event depth not threaded into `while`
10 event depth not threaded into `else`
11 event depth check moved AFTER the list check
12 event line loses its range check
13 MAX_VALUE_DEPTH 128 -> 40
14 depth witness moved back to the event tree
15 a new coordinate-bearing $def, classified by nobody
16 a classified $def loses its coordinate
17 discovery walk narrowed to top-level properties
13 and 14 are the pair worth reading together: 13 was invisible under the old
witness and 14 restores the old witness, so each is the other's guard. 7 and
11 are the same pair for the two recursions.
The campaign was also run once with `git checkout` as its restore step, which
reverted the uncommitted fix along with the mutation and reported anchors
missing and one compile error as a catch. Re-run against file copies. A
mutation harness that cannot tell "the guard caught it" from "the build broke"
measures nothing, and this is the third distinct way that has happened on this
track.
Refs #250, #259.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
The status surfaces move together, so P-022 and the proposals index are the same change; #250 and the PR body follow separately because they live on GitHub. cp1 goes from "acceptance surface closed except two named families" to complete. The row is rewritten rather than edited, because the interesting content changed: there were three censuses, not two, and the third is the one that produced a result worth quoting. What the third census found is recorded, not just its number. Admitting the two excluded families opened 7 permissive documents and 8 category mismatches, and the defect underneath the mismatches was that the ledger had been reading its category off the reference's DIAGNOSTIC rather than off the mechanism — `_check_column` raises one message for a bool, a string, a float, an out-of-range integer and a zero alike, so a bool column was filed as a 1-based-contract violation. The taxonomy is therefore described by its two axes now, not by its seven names. The preferred queue loses its head entry and gains the reason it was there. "Defensive limits first" reads like sequencing preference in hindsight; it was not. The limits changed what the reference ACCEPTS, so they had to land Python-first and cp1 had to be re-measured against them rather than merged beside them. Refs #250, #259. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CJF7MBi1ijU5m9cJVWgQsM
b447e50 to
0738d29
Compare
Что и зачем
#259 checkpoint 1. Не «портировать 47
if'ов», а доказать, что два loader'а принимают один язык допустимых OwnIR-документов и одинаково классифицируют отклонения.Три census'а. Третий — главное, что здесь есть. Первый дал 0/0/0 и не был доказательством. Второй нашёл 58 расхождений и намеренно исключил два семейства. Третий вернул их и нашёл дефект классификации, который был виден в файле и читался как замысел.
Тип изменения
Как проверено
python tests/run_tests.py,ruff check .,mypy(30 файлов)cargo fmt+cargo clippy --workspace --all-targets(0) +cargo test --workspace --no-fail-fast(34 таргета, 0 падений) +cargo doc(0)Python не менялся ни в одном коммите: он здесь oracle, а не предмет правки. Единственное изменение reference'а на этом треке — #326, отдельный Python-first PR, уже в main.
Связанные issue
Refs #250, #259. Ничего не закрывает — cp1 из пяти checkpoint'ов.
Чеклист
Раунд 1: 77 контролей, 0/0/0, и почему это не было доказательством
Первый census заморозил 77 контролей и открылся на 12 Rust-only accepts: шесть полей не были объявлены в модели и проваливались в
serde(flatten) extra. Проверено эмпирически —{"protocols": {"a": 1}}принимался и молча сохранялся.Дальше независимое ревью нашло семь расхождений, которые ledger структурно не мог выразить.
Это провал ledger'а, а не невнимательности. Я написал и oracle, и порт. Один пробел в чтении BR-D1 дал совпадающий пробел в обоих, и матрица согласилась сама с собой. Самый чистый пример — хелпер
_svc(), который всегда проставлялlifetime: ни один контроль не мог выразить его отсутствие.Mutation testing доказывал реализацию против ledger'а. Ledger против контракта не доказывал ничего.
Раунд 2: 193 контроля, выведенных из reference построчно
Перечитывание
load()иownlang/obligations.pyстрока за строкой, до того как смотреть на порт. Хелперы теперь намеренно строят неполные записи.Измеренный RED: 58 Rust-only accepts и 9 category mismatch.
Починка была архитектурной. Старая дверь —
version → все семантические gate → serde для всех shape— это третий порядок проверок, не совпадающий ни с одной реализацией. BR-D1 доводит каждую секцию до конца, перемежая внутри неё shape и семантику. Ни одна перестановка двух проходов не воспроизводит один перемежающийся проход; перемежение должно быть кодом.serde стал конструктором: отказ после принятия валидатором помечается сентинелом и проверяется тестом
no_control_escapes_into_serde.Портирована только acceptance grammar обязательств — то, что дверь принимает. Не портированы решётка, walker, matching, вердикты. Ранее это было записано как «делегированная граница»; ревью было право, а формулировка нет — reference вызывает парсер внутри
load(), так что это была дыра в двери на 47 из 58 permissive-случаев.Добавлена седьмая категория
WellFormedness— для двух правил протокола, где все значения правильного типа и в словаре, а запись всё равно ничего не значит.Раунд 3: два исключённых семейства, и дефект под ними
Раунд 2 честно записал, что исключает два измеренных Python-accept/Rust-reject семейства: координаты вне i64 и глубокую вложенность. Но 0/0/0 на множестве, из которого удалены оба места, где реализации заведомо расходятся, — это утверждение о выбранном подмножестве, а не parity.
#326 закрыл оба Python-first, поэтому причина исключения исчезла. 193 → 216 контролей, и они открыли три разных механизма:
Восемь
line-путей уходили в serde.is_integer()отвечал на вопрос «это вообще целое», аi64::MAX + 1— целое, поэтому сырой слой пропускал значение, а типизированная модель отвергала его потом. Правило жило в модели, а не в двери, отчего и категория, и порядок были случайны.Семь документов reference отвергает, а порт анализировал: шесть контролей вложенности (правила глубины в порту не было вовсе) и
event-line-above-i64, который даже не доходил до сентинела — события хранятся сырыми, serde их не видит.Восемь отвергаются обеими сторонами с разной причиной — и это самая ценная находка.
columnчитал свою категорию из диагностики reference, а не из механизма:_check_columnподнимает одно сообщение и для bool, и для строки, и для float, и для целого вне диапазона, и для нуля. Ledger унаследовал одно сообщение как одну категорию — и bool-колонка былаlocation, то есть «нарушением 1-based контракта» для значения, в котором нет числа, чтобы 1-based правило было о нём.Смешение лежало в файле и читалось как замысел:
column-floatбылlocation,line-floatрядом —shape, с комментарием, объясняющим, что это одно и то же, «только здесь shape». Одно нарушение, две категории, задокументированные как решение.Таксономия: семь категорий на двух осях
Слово representable принадлежит OwnIR, а не serde:
i64::MIN - 1— этоshape, потому что §4.2 объявил signed-64 представимой формой, а не потому что парсер превратил значение в float.Замерено, что парсер приходит к этим значениям двумя разными маршрутами:
i64::MAX+1 ..= u64::MAXматериализуется как u64, всё за пределамиi64::MIN ..= u64::MAXуходит в f64, и отрицательной u64-полосы не существует — то есть концы диапазона не зеркальны. Восстановить потерянный токен можно было бы только черезarbitrary_precision. Одна категория на оба маршрута снимает эту необходимость и, главное, не даёт материализации парсера выбирать семантику.Шесть существующих контролей переехали
location→shape. Python при этом не менялся ни в accept/reject, ни в тексте ошибки — двигается только наша cross-language классификация причины.Проверено до того, как делать: все четыре cross-category
order-*контроля используютcolumn: 0, то есть остаются настоящимиlocation-контролями. Иначе более чистая таксономия была бы куплена ценой обесценивания BR-D1 ordering-доказательства.Depth witness пришлось переносить, и это самое поучительное
the_depth_guard_never_fires_on_a_document_from_json_acceptsстроил дерево событий и шёл вглубь, покаfrom_jsonне откажет. Корректно, пока это дерево ничем не ограничено — а правило вложенности его ограничивает. Обход стал останавливаться на двери вместо парсера, и утверждение тихо выродилось из «guard слабее потолка парсера» в «guard слабее 32».Замерено сразу после появления правила:
Починка из двух половин: witness переехал в неизвестную top-level секцию, и обход теперь утверждает, что остановил его именно
OwnIrErrorKind::Json. Обобщает только вторая половина — выбор неограниченного witness'а есть факт о сегодняшних правилах, и прошлый witness перестал им быть молча.Тем же приёмом закрыта binding-карта схемы: раньше она обходила только те
$def, которые сама называла, поэтому новый координатный$defне попал бы ни в одну сторону и не проверялся бы ничем — утверждение, добросовестно доказывающее полноту списка при помощи этого же списка.Итоговая матрица
Безусловное. Ни одно семейство не исключено.
48 мутаций за три раунда, все пойманы. В третьем раунде 17, из них две пары стоят того, чтобы читать их вместе:
MAX_VALUE_DEPTH 128 → 40была невидима под старым witness'ом, а «вернуть старый witness» — отдельная мутация, так что каждая охраняет другую; и то же самое для двух рекурсий — проверка глубины до/после early return в flow-обходе и в обходе событий стоит в разных местах, потому что так стоит в reference, и превращение любой из них в форму другой ловится.Что осталось незакрытым, и это записано там, где живёт
components[].subscriptions[].lineиlineна flow-операции не валидируютсяload()вообще — ни на диапазон, ни на тип. Замерено,{"line": "x"}принимается обеими реализациями. Это не parity-разрыв, а открытый вопрос контракта, зафиксированный в §4.2. Придумывать здесь контроль означало бы придумывать правило, которого нет ни у одного loader'а.Сбои измерительного инструмента
Раунд 1 трижды получал ложное «мутация выжила»:
cargo build -p own-irсобирает только lib;head -12обрезал вывод; compile-guard грепал^error:, который матчит иerror: test failed.Раунд 2:
grep -c, возвращающий 0, рвёт&&-цепочку и молча пропускаетcargo test --workspace; сорвавшийсяcdоставил бинарный поиск гонять несуществующий таргет.Раунд 3 добавил третий класс: mutation-кампания с
git checkoutв качестве restore откатила вместе с мутацией и сам незакоммиченный фикс, после чего отрапортовала пропавшие якоря и одну ошибку компиляции как «поймано». Перезапущено на копиях файлов. Харнесс, не отличающий «guard поймал» от «сборка сломалась», не измеряет ничего.И отдельный класс, тянущийся через все раунды: doc-комментарии переживают код, который описывают. В этом раунде —
events(), где было написано, что счётчик глубины «никогда не был бы тем, что срабатывает».Generated by Claude Code